es:ES, a:Atom1, i:Id.
i || a
 (e:E.
 (loc(e) = i)
  e'e.e' receives || a & ((first(e'))  es_state_when(es;e'):es_state(es;i)||a)
  (e sends || a & es_state_when(es;e):es_state(es;loc(e))||a)) 

latex

Definitions

{T}, P  Q, x:A. B(x), SQType(T), t  T, s ~ t, Atom$n, {x:A| B(x)} , es_state(es;i), es_state_when(es;e), x:AB(x), es_vartype(es;i;x), x:A  B(x), ES, x:T||a, WellFnd{i}(A;x,y.R(x;y)), t.1, E, (e < e'), (e <loc e'), if b then t else f fi , e sends || a, e receives || a, False, A, e loc e' , P & Q, ee'.P(e), let x,y = A in B(x;y), <a, b>, isrcv(e), P  Q, P  Q, case b of inl(x) => s(x) | inr(y) => t(y), left + right, P  Q, Dec(P), Void, pred(e), , x. t(x), x.A(x), , loc(e), Id, s = t, first(e), b, i || a, Type

Lemmas

es-locl-wellfnd, alle-le wf, free-from-atom wf1, es-atom-axiom, assert wf, es-isrcv wf, es-pred wf, decidable assert, es-le weakening eq, es-isrcv-loc, es-le-loc, es-loc-pred, es-pred-locl, es-locl transitivity1, es-le weakening, es state when wf, Id sq